The update notation for sequences and records generalizes recursively to nested components accessed by “paths” :

$$pth::=([\dots ]|.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}{)}^{+}$$ is sclass="">$$swith[i]pth=A$$ $$swith[i]=(s[i]withpth=A)$$ $$rwith\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}pth=A$$ $$rwith\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=(r.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}withpth=A)$$ is shoclass="">$$rwith.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=A$$ .
class="">$$rwith\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}=A$$ <="index-2">

2.1.3. Vectors

Vectors are bounded sequences of the form (or ), where the can either beclass="">$$A^n$$ $$A^{\ast }$$ $$A$$

$$2^{32}-1$$ $$\begin{array}{r}\begin{array}{lllll}& vec(A)& ::=& A^n& (ifn<2^{32})\end{array}\end{array}$$

2.2. Values

WebAssembly programs operate on primitive numeric values. Moreover, in the definition of programs, immutable sequences of values occur to represent more complex data, such as text strings or other vectors.

2.2.1. Bytes

The simplest form of value are raw uninterpreted bytes. In the abstract syntax they are represented as hexadecimal literals.

$$\begin{array}{r}\begin{array}{llll}& byte& ::=& 0\mathtt{x}00|\dots |0\mathtt{x}\mathtt{F}\mathtt{F}\end{array}\end{array}$$ 2.2.1.1. Conventions

• The meta variable ranges over bytes.
• Bytes are sometimes interpreted as natural numbers $$b$$ .

$$n<256$$

2.2.2. Integers

Different classes of integers with different value ranges are distinguished by their bit width and by whether they are unsigned or signed.

$$N$$ $$\begin{array}{r}\begin{array}{llll}& uN& ::=& 0|1|\dots |2^N-1\\ & sN& ::=& -2^{N-1}|\dots |-1|0|1|\dots |2^{N-1}-1\\ & iN& ::=& uN\end{array}\end{array}$$ convert them to signed based on a two’s complement interpretation.

Note

The main integer types occurring in this specification are , class="">$$u32$$ , class="">$$u64$$ , class="">$$s32$$ , class="">$$s64$$ , $$i8$$ , class="">$$i16$$ , class="">$$i32$$ . class="">$$i64$$ <#syntax-float">floating-point numbers.

2.2.2.1. Conventions

• The meta variables range over integers.
• Numbers may be denoted by simple arithmetics, as in theclass="">$$m,n,i$$ from sequences like , the latter is distinguished with parentheclass="">$$2^N$$

class="">$$(1{)}^N$$

2.2.3. Floating-Point

Floating-point data represents 32 or 64 bit values that correspond to the respective binary formats of the IEEE 754-2008 standard (Section 3.3).

Every value has a sign and a magnitude. Magnitudes can either be expressed as normal numbers of the form , where is the exponent and $$m_0.m_1{m}_2\dots m_M\cdot 2^e$$ $$e$$ is $$m$$ , or as a subnormal number where the exponent is fixed class="">$$m_0$$ $$1$$ is ; among the subnormals are positive and negative zero values. Siclass="">$$m_0$$ $$0$$ , where is the bit width of $$(1+m\cdot 2^{-M})\cdot 2^e$$

Poclass="">$$M$$ $$m$$ (infinity) and $$\infty$$ < a number). NaN values have class="">$$\mathsf{n}\mathsf{a}\mathsf{n}$$ binary representation. No distinction is made between signalling and quiet NaNs.

$$\begin{array}{r}\begin{array}{llcll}& fN& ::=& +fNmag|-fNmag& \\ & fNmag& ::=& (1+uM\cdot 2^{-M})\cdot 2^e& (if-2^{E-1}+2\le e\le 2^{E-1}-1)\\ & & |& (0+uM\cdot 2^{-M})\cdot 2^e& (ife=-2^{E-1}+2)\\ & & |& \infty & \\ & & |& \mathsf{n}\mathsf{a}\mathsf{n}(n)& (if1\le n<2^M)\end{array}\end{array}$$ $$M=\mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}\mathrm{i}\mathrm{f}(N)$$ <

$$E=\mathrm{e}\mathrm{x}\mathrm{p}\mathrm{o}\mathrm{n}(N)$$ <}{lclllllcl} \href{../syntax/valuclass="">

A canonical NaN is a floating-point value $$\pm \mathsf{n}\mathsf{a}\mathsf{n}({\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_N)$$ $${\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_N$$ :

$$1$$ $$0$$ $${\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_N=2^{\mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}\mathrm{i}\mathrm{f}(N)-1}$$ with $$\pm \mathsf{n}\mathsf{a}\mathsf{n}(n)$$ $$n\ge {\mathrm{c}\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{n}}_N$$ <

class="">$$1$$ Note

In the abstract syntax, subnormals are distinguished by the leading 0 of the significand. The exponent of subnormals has the same value as the smallest possible exponent of a normal number. Only in the binary representation the exponent of a subnormal is encoded differently than the exponent of any normal number.

2.2.3.1. Conventions

• The meta variable ranges over floating-point values where clear from context.

class="">$$z$$ <

2.2.4. Names

Names are sequences of scalar code points as defined by Unicode (Section 2.4).

$$\begin{array}{r}\begin{array}{llcl}& name& ::=& {codepoint}^{\ast }(if|\mathrm{u}\mathrm{t}\mathrm{f}8({codepoint}^{\ast })|<2^{32})\\ & codepoint& ::=& \mathrm{U}+00|\dots |\mathrm{U}+\mathrm{D}7\mathrm{F}\mathrm{F}|\mathrm{U}+\mathrm{E}000|\dots |\mathrm{U}+10\mathrm{F}\mathrm{F}\mathrm{F}\mathrm{F}\end{array}\end{array}$$ binary format, the lengths of a name is bounded by the length of its UTF-8 encoding.

2.2.4.1. Convention

• Code points are sometimes used interchangeably with natural numbers .

$$n<1114112$$

2.3. Types

Various entitites in WebAssembly are classified by types. Types are checked during validation, instantiation, and possibly execution.

2.3.1. Value Types

Value types classify the individual values that WebAssembly code can compute with and the values that a variable accepts.

$$\begin{array}{r}\begin{array}{llll}& valtype& ::=& \mathsf{i}32|\mathsf{i}64|\mathsf{f}32|\mathsf{f}64\end{array}\end{array}$$ $$\mathsf{i}32$$ $$\mathsf{i}64$$

The types and $$\mathsf{f}32$$ $$\mathsf{f}64$$ single and double precision, as defined by the IEEE 754-2008 standard (Section 3.3).

2.3.1.1. Conventions

• The meta variable ranges over value types where clear from context.
• The notation $$t$$ bit width of a value type. That is, $$|t|$$ $$|\mathsf{i}32|=|\mathsf{f}32|=32$$ $$|\mathsf{i}64|=|\mathsf{f}64|=64$$ <

  2.3.2. Result Types

  Result types classify the result of executing instructions or blocks, which is a sequence of values.

  $$\begin{array}{r}\begin{array}{llll}& resulttype& ::=& [{valtype}^{?}]\end{array}\end{array}$$ <

  In the current version of WebAssembly, at most one value is allowed as a result. However, this may be generalized to sequences of values in future versions.

2.3.3. Function Types

Function types classify the signature of functions, mapping a vector of parameters to a vector of results.

$$\begin{array}{r}\begin{array}{llll}& functype& ::=& [vec(valtype)]\to [vec(valtype)]\end{array}\end{array}$$ <

In the current version of WebAssembly, the length of the result type vector of a valid function type may be at most . This restriction may be removed in future versions.

class="">$$1$$

2.3.4. Limits

Limits classify the size range of resizeable storage associated with memory types and table types.

$$\begin{array}{r}\begin{array}{llll}& limits& ::=& \{\mathsf{m}\mathsf{i}\mathsf{n}u32,\mathsf{m}\mathsf{a}\mathsf{x}{u32}^{?}\}\end{array}\end{array}$$

2.3.5. Memory Types

Memory types classify linear memories and their size range.

$$\begin{array}{r}\begin{array}{llll}& memtype& ::=& limits\end{array}\end{array}$$ page size.

2.3.6. Table Types

Table types classify tables over elements of element types within a size range.

$$\begin{array}{r}\begin{array}{llll}& tabletype& ::=& limitselemtype\\ & elemtype& ::=& \mathsf{a}\mathsf{n}\mathsf{y}\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\end{array}\end{array}$$ < are given in numbers of entries.

The element type is the infinite union of all $$\mathsf{a}\mathsf{n}\mathsf{y}\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}$$ . A table of that type thus contains references to functions of heterogeneous type.

Note

In future versions of WebAssembly, additional element types may be introduced.

2.3.7. Global Types

Global types classify global variables, which hold a value and can either be mutable or immutable.

$$\begin{array}{r}\begin{array}{llll}& globaltype& ::=& mutvaltype\\ & mut& ::=& \mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}|\mathsf{v}\mathsf{a}\mathsf{r}\end{array}\end{array}$$ <

2.3.8. External Types

External types classify imports and external values with their respective types.

$$\begin{array}{r}\begin{array}{llll}& externtype& ::=& \mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}functype|\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}tabletype|\mathsf{m}\mathsf{e}\mathsf{m}memtype|\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globaltype\end{array}\end{array}$$ 2.3.8.1. Conventions

The following auxiliary notation is defined for sequences of external types. It filters out entries of a specific kind in an order-preserving fashion:

• $$\mathrm{f}\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{s}({externtype}^{\ast })=[functype|(\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}functype)\in {externtype}^{\ast }]$$ $$\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}({externtype}^{\ast })=[tabletype|(\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}tabletype)\in {externtype}^{\ast }]$$ $$\mathrm{m}\mathrm{e}\mathrm{m}\mathrm{s}({externtype}^{\ast })=[memtype|(\mathsf{m}\mathsf{e}\mathsf{m}memtype)\in {externtype}^{\ast }]$$ $$\mathrm{g}\mathrm{l}\mathrm{o}\mathrm{b}\mathrm{a}\mathrm{l}\mathrm{s}({externtype}^{\ast })=[globaltype|(\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globaltype)\in {externtype}^{\ast }]$$

  2.4. Instructions

  WebAssembly code consists of sequences of instructions. Its computational model is based on a stack machine in that instructions manipulate values on an implicit operand stack, consuming (popping) argument values and producing (pushing) result values.

  Note

  In the current version of WebAssembly, at most one result value can be pushed by a single instruction. This restriction may be lifted in future versions.

  In addition to dynamic operands from the stack, some instructions also have static immediate arguments, typically indices or type annotations, which are part of the instruction itself.

  Some instructions are structured in that they bracket nested sequences of instructions.

  The following sections group instructions into a number of different categories.

  2.4.1. Numeric Instructions

  Numeric instructions provide basic operations over numeric values of specific type. These operations closely match respective operations available in hardware.

  $$\begin{array}{r}\begin{array}{llcl}& nn,mm& ::=& 32|64\\ & sx& ::=& \mathsf{u}|\mathsf{s}\\ & instr& ::=& \mathsf{i}nn.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}inn|\mathsf{f}nn.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}fnn\\ & & |& \mathsf{i}nn.iunop|\mathsf{f}nn.funop\\ & & |& \mathsf{i}nn.ibinop|\mathsf{f}nn.fbinop\\ & & |& \mathsf{i}nn.itestop\\ & & |& \mathsf{i}nn.irelop|\mathsf{f}nn.frelop\\ & & |& \mathsf{i}32.\mathsf{w}\mathsf{r}\mathsf{a}\mathsf{p}/\mathsf{i}64|\mathsf{i}64.\mathsf{e}\mathsf{x}\mathsf{t}\mathsf{e}\mathsf{n}\mathsf{d}\_sx/\mathsf{i}32|\mathsf{i}nn.\mathsf{t}\mathsf{r}\mathsf{u}\mathsf{n}\mathsf{c}\_sx/\mathsf{f}mm\\ & & |& \mathsf{f}32.\mathsf{d}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{t}\mathsf{e}/\mathsf{f}64|\mathsf{f}64.\mathsf{p}\mathsf{r}\mathsf{o}\mathsf{m}\mathsf{o}\mathsf{t}\mathsf{e}/\mathsf{f}32|\mathsf{f}nn.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{v}\mathsf{e}\mathsf{r}\mathsf{t}\_sx/\mathsf{i}mm\\ & & |& \mathsf{i}nn.\mathsf{r}\mathsf{e}\mathsf{i}\mathsf{n}\mathsf{t}\mathsf{e}\mathsf{r}\mathsf{p}\mathsf{r}\mathsf{e}\mathsf{t}/\mathsf{f}nn|\mathsf{f}nn.\mathsf{r}\mathsf{e}\mathsf{i}\mathsf{n}\mathsf{t}\mathsf{e}\mathsf{r}\mathsf{p}\mathsf{r}\mathsf{e}\mathsf{t}/\mathsf{i}nn\\ & iunop& ::=& \mathsf{c}\mathsf{l}\mathsf{z}|\mathsf{c}\mathsf{t}\mathsf{z}|\mathsf{p}\mathsf{o}\mathsf{p}\mathsf{c}\mathsf{n}\mathsf{t}\\ & ibinop& ::=& \mathsf{a}\mathsf{d}\mathsf{d}|\mathsf{s}\mathsf{u}\mathsf{b}|\mathsf{m}\mathsf{u}\mathsf{l}|\mathsf{d}\mathsf{i}\mathsf{v}\_sx|\mathsf{r}\mathsf{e}\mathsf{m}\_sx\\ & & |& \mathsf{a}\mathsf{n}\mathsf{d}|\mathsf{o}\mathsf{r}|\mathsf{x}\mathsf{o}\mathsf{r}|\mathsf{s}\mathsf{h}\mathsf{l}|\mathsf{s}\mathsf{h}\mathsf{r}\_sx|\mathsf{r}\mathsf{o}\mathsf{t}\mathsf{l}|\mathsf{r}\mathsf{o}\mathsf{t}\mathsf{r}\\ & funop& ::=& \mathsf{a}\mathsf{b}\mathsf{s}|\mathsf{n}\mathsf{e}\mathsf{g}|\mathsf{s}\mathsf{q}\mathsf{r}\mathsf{t}|\mathsf{c}\mathsf{e}\mathsf{i}\mathsf{l}|\mathsf{f}\mathsf{l}\mathsf{o}\mathsf{o}\mathsf{r}|\mathsf{t}\mathsf{r}\mathsf{u}\mathsf{n}\mathsf{c}|\mathsf{n}\mathsf{e}\mathsf{a}\mathsf{r}\mathsf{e}\mathsf{s}\mathsf{t}\\ & fbinop& ::=& \mathsf{a}\mathsf{d}\mathsf{d}|\mathsf{s}\mathsf{u}\mathsf{b}|\mathsf{m}\mathsf{u}\mathsf{l}|\mathsf{d}\mathsf{i}\mathsf{v}|\mathsf{m}\mathsf{i}\mathsf{n}|\mathsf{m}\mathsf{a}\mathsf{x}|\mathsf{c}\mathsf{o}\mathsf{p}\mathsf{y}\mathsf{s}\mathsf{i}\mathsf{g}\mathsf{n}\\ & itestop& ::=& \mathsf{e}\mathsf{q}\mathsf{z}\\ & irelop& ::=& \mathsf{e}\mathsf{q}|\mathsf{n}\mathsf{e}|\mathsf{l}\mathsf{t}\_sx|\mathsf{g}\mathsf{t}\_sx|\mathsf{l}\mathsf{e}\_sx|\mathsf{g}\mathsf{e}\_sx\\ & frelop& ::=& \mathsf{e}\mathsf{q}|\mathsf{n}\mathsf{e}|\mathsf{l}\mathsf{t}|\mathsf{g}\mathsf{t}|\mathsf{l}\mathsf{e}|\mathsf{g}\mathsf{e}\end{array}\end{array}$$ value type. For each type, several subcategories can be distinguished:

  • Constants: return a static constant.
  • Unary Operators: consume one operand and produce one result of the respective type.
  • Binary Operators: consume two operands and produce one result of the respective type.
  • Tests: consume one operand of the respective type and produce a Boolean integer result.
  • Comparisons: consume two operands of the respective type and produce a Boolean integer result.
  • Conversions: consume a value of one type and produce a result of another (the source type of the conversion is the one after the “”).

  Some integer instructions come in two flavours, whereclass="">$$/$$ distinguishes whether the operands are to beclass="">$$sx$$ interpreted as unsigned or signed integers. For the other integer instructions, the use of two’s complement for the signed interpretation means that they behave the same regardless of signedness.

  2.4.1.1. Conventions

  Occasionally, it is convenient to group operators together according to the following grammar shorthands:

  $$\begin{array}{r}\begin{array}{llll}& unop& ::=& iunop|funop\\ & binop& ::=& ibinop|fbinop\\ & testop& ::=& itestop\\ & relop& ::=& irelop|frelop\\ & cvtop& ::=& \mathsf{w}\mathsf{r}\mathsf{a}\mathsf{p}|\mathsf{e}\mathsf{x}\mathsf{t}\mathsf{e}\mathsf{n}\mathsf{d}\_sx|\mathsf{t}\mathsf{r}\mathsf{u}\mathsf{n}\mathsf{c}\_sx|\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{v}\mathsf{e}\mathsf{r}\mathsf{t}\_sx|\mathsf{d}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{t}\mathsf{e}|\mathsf{p}\mathsf{r}\mathsf{o}\mathsf{m}\mathsf{o}\mathsf{t}\mathsf{e}|\mathsf{r}\mathsf{e}\mathsf{i}\mathsf{n}\mathsf{t}\mathsf{e}\mathsf{r}\mathsf{p}\mathsf{r}\mathsf{e}\mathsf{t}\end{array}\end{array}$$ <="syntax-instr-parametric">

  2.4.2. Parametric Instructions

  Instructions in this group can operate on operands of any value type.

  $$\begin{array}{r}\begin{array}{llcl}& instr& ::=& \dots \\ & & |& \mathsf{d}\mathsf{r}\mathsf{o}\mathsf{p}\\ & & |& \mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}\end{array}\end{array}$$ operator simply throws away class="">$$\mathsf{d}\mathsf{r}\mathsf{o}\mathsf{p}$$ operator selects one of itclass="">$$\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ <

  2.4.3. Variable Instructions

  Variable instructions are concerned with the access to local or global variables.

  $$\begin{array}{r}\begin{array}{llcl}& instr& ::=& \dots \\ & & |& \mathsf{g}\mathsf{e}\mathsf{t}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}localidx\\ & & |& \mathsf{s}\mathsf{e}\mathsf{t}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}localidx\\ & & |& \mathsf{t}\mathsf{e}\mathsf{e}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}localidx\\ & & |& \mathsf{g}\mathsf{e}\mathsf{t}\_\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globalidx\\ & & |& \mathsf{s}\mathsf{e}\mathsf{t}\_\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globalidx\end{array}\end{array}$$ instruction is like $$\mathsf{t}\mathsf{e}\mathsf{e}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}$$ but also returns its argclass="">$$\mathsf{s}\mathsf{e}\mathsf{t}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}$$ <

  2.4.4. Memory Instructions

  Instructions in this group are concerned with linear memory.

  $$\begin{array}{r}\begin{array}{llcl}& memarg& ::=& \{\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}u32,\mathsf{a}\mathsf{l}\mathsf{i}\mathsf{g}\mathsf{n}u32\}\\ & instr& ::=& \dots \\ & & |& \mathsf{i}nn.\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}memarg|\mathsf{f}nn.\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}memarg\\ & & |& \mathsf{i}nn.\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}memarg|\mathsf{f}nn.\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}memarg\\ & & |& \mathsf{i}nn.\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}8\_sxmemarg|\mathsf{i}nn.\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}16\_sxmemarg|\mathsf{i}64.\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}32\_sxmemarg\\ & & |& \mathsf{i}nn.\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}8memarg|\mathsf{i}nn.\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}16memarg|\mathsf{i}64.\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}32memarg\\ & & |& \mathsf{c}\mathsf{u}\mathsf{r}\mathsf{r}\mathsf{e}\mathsf{n}\mathsf{t}\_\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{r}\mathsf{y}\\ & & |& \mathsf{g}\mathsf{r}\mathsf{o}\mathsf{w}\_\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{r}\mathsf{y}\end{array}\end{array}$$ and $$\mathsf{l}\mathsf{o}\mathsf{a}\mathsf{d}$$ $$\mathsf{s}\mathsf{t}\mathsf{o}\mathsf{r}\mathsf{e}$$ <>value types. They all take a memory immediate that contains an address offset$$memarg$$ < loads and stores can optionally specify a storage size that is smaller than the bit width of the respective value type. In the case of loads, a sign extension mode is then required to select appropriate behavclass="">$$sx$$ effective address that is the zero-based index at which the memory is accessed. All values are read and written in little endian byte order. A trap results if any of the accessed memory bytes lies outside the address range implied by the memory’s current size.

  Note

  Future version of WebAssembly might provide memory instructions with 64 bit address ranges.

  The instruction returns tclass="">$$\mathsf{c}\mathsf{u}\mathsf{r}\mathsf{r}\mathsf{e}\mathsf{n}\mathsf{t}\_\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{r}\mathsf{y}$$ instruction grows memoryclass="">$$\mathsf{g}\mathsf{r}\mathsf{o}\mathsf{w}\_\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{o}\mathsf{r}\mathsf{y}$$ $$-1$$ page size.

  Note

  In the current version of WebAssembly, all memory instructions implicitly operate on memory index . This restriction may be lifted in future versions.

  class="">$$0$$

  2.4.5. Control Instructions

  Instructions in this group affect the flow of control.

  $$\begin{array}{r}\begin{array}{llcl}& instr& ::=& \dots \\ & & |& \mathsf{n}\mathsf{o}\mathsf{p}\\ & & |& \mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}\\ & & |& \mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}resulttype{instr}^{\ast }\mathsf{e}\mathsf{n}\mathsf{d}\\ & & |& \mathsf{l}\mathsf{o}\mathsf{o}\mathsf{p}resulttype{instr}^{\ast }\mathsf{e}\mathsf{n}\mathsf{d}\\ & & |& \mathsf{i}\mathsf{f}resulttype{instr}^{\ast }\mathsf{e}\mathsf{l}\mathsf{s}\mathsf{e}{instr}^{\ast }\mathsf{e}\mathsf{n}\mathsf{d}\\ & & |& \mathsf{b}\mathsf{r}labelidx\\ & & |& \mathsf{b}\mathsf{r}\_\mathsf{i}\mathsf{f}labelidx\\ & & |& \mathsf{b}\mathsf{r}\_\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}vec(labelidx)labelidx\\ & & |& \mathsf{r}\mathsf{e}\mathsf{t}\mathsf{u}\mathsf{r}\mathsf{n}\\ & & |& \mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}funcidx\\ & & |& \mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}\_\mathsf{i}\mathsf{n}\mathsf{d}\mathsf{i}\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{t}typeidx\end{array}\end{array}$$ class="">$$\mathsf{n}\mathsf{o}\mathsf{p}$$ instruction causes an unclass="">$$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ <.

  The , $$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$ $$\mathsf{l}\mathsf{o}\mathsf{o}\mathsf{p}$$ < structured$$\mathsf{i}\mathsf{f}$$ <>, terminated with, or separated by, or $$\mathsf{e}\mathsf{n}\mathsf{d}$$ $$\mathsf{e}\mathsf{l}\mathsf{s}\mathsf{e}$$ result type.

  Each structured control instruction introduces an implicit label. Labels are targets for branch instructions that reference them with label indices. Unlike with other index spaces, indexing of labels is relative by nesting depth, that is, label refers to the innermost structured control instruction enclosing the referring branch instruction, wclass="">$$0$$ within the associated structured control instruction. This also implies that branches can only be directed outwards, “breaking” from the block of the control construct they target. The exact effect depends on that control construct. In case of or $$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$ , reclass="">$$\mathsf{i}\mathsf{f}$$ . In case of $$\mathsf{e}\mathsf{n}\mathsf{d}$$ backward jump class="">$$\mathsf{l}\mathsf{o}\mathsf{o}\mathsf{p}$$ <

  Note

  This enforces structured control flow. Intuitively, a branch targeting a or $$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$ $$\mathsf{i}\mathsf{f}$$ $$\mathsf{b}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{k}$$ behaves like a $$\mathsf{l}\mathsf{o}\mathsf{o}\mathsf{p}$$ $$\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{t}\mathsf{i}\mathsf{n}\mathsf{u}\mathsf{e}$$ performs an unconditional branch,class="">$$\mathsf{b}\mathsf{r}$$ performs a conditional branchclass="">$$\mathsf{b}\mathsf{r}\_\mathsf{i}\mathsf{f}$$ performs an indirect brancclass="">$$\mathsf{b}\mathsf{r}\_\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ instruction is a shortcut forclass="">$$\mathsf{r}\mathsf{e}\mathsf{t}\mathsf{u}\mathsf{r}\mathsf{n}$$ unwinds the operand stack up to the height where the targeted structured control instruction was entered. However, forward branches that target a control instruction with a non-empty result type consume matching operands first and push them back on the operand stack after unwinding, as a result for the terminated structured instruction.

  The instruction invokes another $$\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}$$ , consuming the necessary arguments from the stack and returning the result values of the call. The instruction calls a fclass="">$$\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}\_\mathsf{i}\mathsf{n}\mathsf{d}\mathsf{i}\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{t}$$ table. Since tables may contain function elements of heterogeneous type , the callee is dynamically checked againclass="">$$\mathsf{a}\mathsf{n}\mathsf{y}\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}$$ function type indexed by the instruction’s immediate, and the call aborted with a trap if it does not match.

  Note

  In the current version of WebAssembly, implicitly operates oclass="">$$\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{l}\_\mathsf{i}\mathsf{n}\mathsf{d}\mathsf{i}\mathsf{r}\mathsf{e}\mathsf{c}\mathsf{t}$$ index . This restriction may be lifted in future versions.

  class="">$$0$$

  2.4.6. Expressions

  Function bodies, initialization values for globals, and offsets of element or data segments are given as expressions, which are sequences of instructions terminated by an marker.

  $$\mathsf{e}\mathsf{n}\mathsf{d}$$ $$\begin{array}{r}\begin{array}{llll}& expr& ::=& {instr}^{\ast }\mathsf{e}\mathsf{n}\mathsf{d}\end{array}\end{array}$$ restricts expressions to be constant, which limits the set of allowable instructions.

  2.5. Modules

  WebAssembly programs are organized into modules, which are the unit of deployment, loading, and compilation. A module collects definitions for types, functions, tables, memories, and globals. In addition, it can declare imports and exports and provide initialization logic in the form of data and element segments or a start function.

  $$\begin{array}{r}\begin{array}{lllll}& module& ::=& \{& \mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}\mathsf{s}vec(functype),\\ & & & & \mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\mathsf{s}vec(func),\\ & & & & \mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}\mathsf{s}vec(table),\\ & & & & \mathsf{m}\mathsf{e}\mathsf{m}\mathsf{s}vec(mem),\\ & & & & \mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}\mathsf{s}vec(global),\\ & & & & \mathsf{e}\mathsf{l}\mathsf{e}\mathsf{m}vec(elem),\\ & & & & \mathsf{d}\mathsf{a}\mathsf{t}\mathsf{a}vec(data),\\ & & & & \mathsf{s}\mathsf{t}\mathsf{a}\mathsf{r}\mathsf{t}{start}^{?},\\ & & & & \mathsf{i}\mathsf{m}\mathsf{p}\mathsf{o}\mathsf{r}\mathsf{t}\mathsf{s}vec(import),\\ & & & & \mathsf{e}\mathsf{x}\mathsf{p}\mathsf{o}\mathsf{r}\mathsf{t}\mathsf{s}vec(export)\}\end{array}\end{array}$$

  2.5.1. Indices

  Definitions are referenced with zero-based indices. Each class of definition has its own index space, as distinguished by the following classes.

  $$\begin{array}{r}\begin{array}{llll}& typeidx& ::=& u32\\ & funcidx& ::=& u32\\ & tableidx& ::=& u32\\ & memidx& ::=& u32\\ & globalidx& ::=& u32\\ & localidx& ::=& u32\\ & labelidx& ::=& u32\end{array}\end{array}$$ <, tables, memories and globals includes respective imports declared in the same module. The indices of these imports precede the indices of other definitions in the same index space.

  The index space for locals is only accessible inside a function and includes the parameters and local variables of that function, which precede the other locals.

  Label indices reference structured control instructions inside an instruction sequence.

  2.5.1.1. Conventions

  • The meta variable ranges over label indices.
  • The meta variables rclass="">$$l$$

  class="">$$x,y$$ <

  2.5.2. Types

  The component of a module defines a vector of class="">$$\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}\mathsf{s}$$ function types.

  All function types used in a module must be defined in this component. They are referenced by type indices.

  Note

  Future versions of WebAssembly may add additional forms of type definitions.

  2.5.3. Functions

  The component of a module defines a vector of class="">$$\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\mathsf{s}$$ $$\begin{array}{r}\begin{array}{llll}& func& ::=& \{\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}typeidx,\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{s}vec(valtype),\mathsf{b}\mathsf{o}\mathsf{d}\mathsf{y}expr\}\end{array}\end{array}$$ $$\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}$$ type defined in the module. The parameters of the function are referenced through 0-based local indices in the function’s body.

  The declare a vector of mutable local variablesclass="">$$\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{s}$$ < internal" href="#syntax-localidx">local indices in the function’s body. The index of the first local is the smallest index not referencing a parameter.

  The is an $$\mathsf{b}\mathsf{o}\mathsf{d}\mathsf{y}$$ result type.

  Functions are referenced through function indices, starting with the smallest index not referencing a function import.

  2.5.4. Tables

  The component of a module defines a vector ofclass="">$$\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}\mathsf{s}$$ table type:

  $$\begin{array}{r}\begin{array}{llll}& table& ::=& \{\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}tabletype\}\end{array}\end{array}$$ <#syntax-elemtype">element type. The size in the $$\mathsf{m}\mathsf{i}\mathsf{n}$$ , if present, restricts the size to which it caclass="">$$\mathsf{m}\mathsf{a}\mathsf{x}$$ element segments.

  Tables are referenced through table indices, starting with the smallest index not referencing a table import. Most constructs implicitly reference table index .

  $$0$$ <

  In the current version of WebAssembly, at most one table may be defined or imported in a single module, and all constructs implicitly reference this table . This restriction may be lifted in future versions.

  class="">$$0$$

  2.5.5. Memories

  The component of a module defines a vector of $$\mathsf{m}\mathsf{e}\mathsf{m}\mathsf{s}$$ memory type:

  $$\begin{array}{r}\begin{array}{llll}& mem& ::=& \{\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}memtype\}\end{array}\end{array}$$ size in the $$\mathsf{m}\mathsf{i}\mathsf{n}$$ , if present, restricts the size to which it caclass="">$$\mathsf{m}\mathsf{a}\mathsf{x}$$ page size.

  Memories can be initialized through data segments.

  Memories are referenced through memory indices, starting with the smallest index not referencing a memory import. Most constructs implicitly reference memory index .

  $$0$$ <

  In the current version of WebAssembly, at most one memory may be defined or imported in a single module, and all constructs implicitly reference this memory . This restriction may be lifted in future versions.

  class="">$$0$$

  2.5.6. Globals

  The component of a module defines a vector oclass="">$$\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}\mathsf{s}$$ $$\begin{array}{r}\begin{array}{llll}& global& ::=& \{\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}globaltype,\mathsf{i}\mathsf{n}\mathsf{i}\mathsf{t}expr\}\end{array}\end{array}$$ global type. Its also specifies whether a global is immutablclass="">$$\mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}$$ value given by a $$\mathsf{i}\mathsf{n}\mathsf{i}\mathsf{t}$$ initializer expression.

  Globals are referenced through global indices, starting with the smallest index not referencing a global import.

  2.5.7. Element Segments

  The initial contents of a table is uninitialized. The component of a module defines a vector of $$\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{m}$$ vector of elements.

  $$\begin{array}{r}\begin{array}{llll}& elem& ::=& \{\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}tableidx,\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}expr,\mathsf{i}\mathsf{n}\mathsf{i}\mathsf{t}vec(funcidx)\}\end{array}\end{array}$$ $$\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}$$ expression.

  Note

  In the current version of WebAssembly, at most one table is allowed in a module. Consequently, the only valid is .$$tableidx$$ class="">$$0$$

  2.5.8. Data Segments

  The initial contents of a memory are zero bytes. The component of a module defines a vector of $$\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{a}$$ vector of bytes.

  $$\begin{array}{r}\begin{array}{llll}& data& ::=& \{\mathsf{d}\mathsf{a}\mathsf{t}\mathsf{a}memidx,\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}expr,\mathsf{i}\mathsf{n}\mathsf{i}\mathsf{t}vec(byte)\}\end{array}\end{array}$$ $$\mathsf{o}\mathsf{f}\mathsf{f}\mathsf{s}\mathsf{e}\mathsf{t}$$ expression.

  Note

  In the current version of WebAssembly, at most one memory is allowed in a module. Consequently, the only valid is .

  class="">$$memidx$$ class="">$$0$$

  2.5.9. Start Function

  The component of a module optionally declares class="">$$\mathsf{s}\mathsf{t}\mathsf{a}\mathsf{r}\mathsf{t}$$ <-ref">function index of a start function that is automatically invoked when the module is instantiated, after tables and memories have been initialized.

  $$\begin{array}{r}\begin{array}{llll}& start& ::=& \{\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}funcidx\}\end{array}\end{array}$$

  2.5.10. Exports

  The component of a module defines a set of $$\mathsf{e}\mathsf{x}\mathsf{p}\mathsf{o}\mathsf{r}\mathsf{t}\mathsf{s}$$ instantiated.

  $$\begin{array}{r}\begin{array}{llcl}& export& ::=& \{\mathsf{n}\mathsf{a}\mathsf{m}\mathsf{e}name,\mathsf{d}\mathsf{e}\mathsf{s}\mathsf{c}exportdesc\}\\ & exportdesc& ::=& \mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}funcidx\\ & & |& \mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}tableidx\\ & & |& \mathsf{m}\mathsf{e}\mathsf{m}memidx\\ & & |& \mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globalidx\end{array}\end{array}$$ name. Exportable definitions are functions, tables, memories, and globals, which are referenced through a respective descriptor.

  Note

  In the current version of WebAssembly, only immutable globals may be exported.

  2.5.10.1. Conventions

  The following auxiliary notation is defined for sequences of exports, filtering out indices of a specific kind in an order-preserving fashion:

  • $$\mathrm{f}\mathrm{u}\mathrm{n}\mathrm{c}\mathrm{s}({export}^{\ast })=[funcidx|\mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}funcidx\in (export.\mathsf{d}\mathsf{e}\mathsf{s}\mathsf{c}{)}^{\ast }]$$ $$\mathrm{t}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}({export}^{\ast })=[tableidx|\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}tableidx\in (export.\mathsf{d}\mathsf{e}\mathsf{s}\mathsf{c}{)}^{\ast }]$$ $$\mathrm{m}\mathrm{e}\mathrm{m}\mathrm{s}({export}^{\ast })=[memidx|\mathsf{m}\mathsf{e}\mathsf{m}memidx\in (export.\mathsf{d}\mathsf{e}\mathsf{s}\mathsf{c}{)}^{\ast }]$$ $$\mathrm{g}\mathrm{l}\mathrm{o}\mathrm{b}\mathrm{a}\mathrm{l}\mathrm{s}({export}^{\ast })=[globalidx|\mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globalidx\in (export.\mathsf{d}\mathsf{e}\mathsf{s}\mathsf{c}{)}^{\ast }]$$

    2.5.11. Imports

    The component of a module defines a set of $$\mathsf{i}\mathsf{m}\mathsf{p}\mathsf{o}\mathsf{r}\mathsf{t}\mathsf{s}$$ <.html#exec-instantiation">instantiation.

    $$\begin{array}{r}\begin{array}{llll}& import& ::=& \{\mathsf{m}\mathsf{o}\mathsf{d}\mathsf{u}\mathsf{l}\mathsf{e}name,\mathsf{n}\mathsf{a}\mathsf{m}\mathsf{e}name,\mathsf{d}\mathsf{e}\mathsf{s}\mathsf{c}importdesc\}\\ & importdesc& ::=& \mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}typeidx\\ & & |& \mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}tabletype\\ & & |& \mathsf{m}\mathsf{e}\mathsf{m}memtype\\ & & |& \mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}globaltype\end{array}\end{array}$$ name space, consisting of a name and a unique $$\mathsf{m}\mathsf{o}\mathsf{d}\mathsf{u}\mathsf{l}\mathsf{e}$$ $$\mathsf{n}\mathsf{a}\mathsf{m}\mathsf{e}$$ functions, tables, memories, and globals. Each import is specified by a descriptor with a respective type that a definition provided during instantiation is required to match.

    Every import defines an index in the respective index space. In each index space, the indices of imports go before the first index of any definition contained in the module itself.

    Note

    In the current version of WebAssembly, only immutable globals may be imported.

  3. Validation

  3.1. Conventions

  Validation checks that a WebAssembly module is well-formed. Only valid modules can be instantiated.

  Validity is defined by a type system over the abstract syntax of a module and its contents. For each piece of abstract syntax, there is a typing rule that specifies the constraints that apply to it. All rules are given in two equivalent forms:

  1. In prose, describing the meaning in intuitive form.
  2. In formal notation, describing the rule in mathematical form. [1]

  Note

  The prose and formal rules are equivalent, so that understanding of the formal notation is not required to read this specification. The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof.

  In both cases, the rules are formulated in a declarative manner. That is, they only formulate the constraints, they do not define an algorithm. The skeleton of a sound and complete algorithm for type-checking instruction sequences according to this specification is provided in the appendix.

  3.1.1. Contexts

  Validity of an individual definition is specified relative to a context, which collects relevant information about the surrounding module and the definitions in scope:

  • Types: the list of types defined in the current module.
  • Functions: the list of functions declared in the current module, represented by their function type.
  • Tables: the list of tables declared in the current module, represented by their table type.
  • Memories: the list of memories declared in the current module, represented by their memory type.
  • Globals: the list of globals declared in the current module, represented by their global type.
  • Locals: the list of locals declared in the current function (including parameters), represented by their value type.
  • Labels: the stack of labels accessible from the current position, represented by their result type.
  • Return: the return type of the current function, represented as a result type.

  In other words, a context contains a sequence of suitable types for each index space, describing each defined entry in that space. Locals, labels and return type are only used for validating instructions in function bodies, and are left empty elsewhere. The label stack is the only part of the context that changes as validation of an instruction sequence proceeds.

  It is convenient to define contexts as records with abstract syntax:

  $$C$$ $$\begin{array}{r}\begin{array}{llll}& C& ::=& \begin{array}{lll}\{& \mathsf{t}\mathsf{y}\mathsf{p}\mathsf{e}\mathsf{s}& {functype}^{\ast },\\ & \mathsf{f}\mathsf{u}\mathsf{n}\mathsf{c}\mathsf{s}& {functype}^{\ast },\\ & \mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}\mathsf{s}& {tabletype}^{\ast },\\ & \mathsf{m}\mathsf{e}\mathsf{m}\mathsf{s}& {memtype}^{\ast },\\ & \mathsf{g}\mathsf{l}\mathsf{o}\mathsf{b}\mathsf{a}\mathsf{l}\mathsf{s}& {globaltype}^{\ast },\\ & \mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{s}& {valtype}^{\ast },\\ & \mathsf{l}\mathsf{a}\mathsf{b}\mathsf{e}\mathsf{l}\mathsf{s}& {resulttype}^{\ast },\\ & \mathsf{r}\mathsf{e}\mathsf{t}\mathsf{u}\mathsf{r}\mathsf{n}& {resulttype}^{?}\}\end{array}\end{array}\end{array}$$ <

  The fields of a context are not defined as vectors, since their lengths are not bounded by the maximum vector size.

  In addition to field access the following notation is adopted for manipulating contexts:

  $$C.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ denotes the same context as but with the elemclass="">$$C,\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}{A}^{\ast }$$ $$C$$ <> component sequence. $$A^{\ast }$$ $$\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ Note

  This notation is defined to prepend not append. It is only used in situations where the original is either empty or is $$C.\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ $$\mathsf{f}\mathsf{i}\mathsf{e}\mathsf{l}\mathsf{d}$$ $$\mathsf{l}\mathsf{a}\mathsf{b}\mathsf{e}\mathsf{l}\mathsf{s}$$ label index space is indexed relatively, that is, in reverse order of addition.

  3.1.2. Prose Notation

  Validation is specified by stylised rules for each relevant part of the abstract syntax. The rules not only state constraints defining when a phrase is valid, they also classify it with a type. The following conventions are adopted in stating these rules.

  • A phrase is said to be “valid with type ” if and only if all constraints eclass="">$$A$$ $$T$$ <> depends on what is.

    $$T$$ <

    $$A$$

    For example, if is a function$$A$$ is a functclass="">$$T$$ <; for an that is a glclass="">$$A$$ is a gloclass="">$$T$$ <; and so on.

  • The rules implicitly assume a given context .

  • In some places, this context is locally extendclass="">$$C$$ with additional entries. The formulation “Under context , … $$C^{\prime }$$ <�� is adopted to express that the following statement must apply under class="">$$C^{\prime }$$

  3.1.3. Formal Notation

  Note

  This section gives a brief explanation of the notation for specifying typing rules formally. For the interested reader, a more thorough introduction can be found in respective text books. [2]

  The proposition that a phrase has a respective type is written class="">$$A$$ $$T$$ . To expreclass="">$$A:T$$ < complete form is a judgement $$C$$ holds under the assumptions encodeclass="">$$C⊢A:T$$ .

  The fclass="">$$A:T$$ $$C$$ deduction rules. Every rule has the following general form:

  $$\frac{{premise}_1{premise}_2\dots {premise}_n}{conclusion}$$ axioms whose conclusion holds unconditionally. The conclusion always is a judgment , and there is one respective rule for each relevant construct $$C⊢A:T$$

  $$A$$ Note

  For example, the typing rule for the $$\mathsf{i}32.\mathsf{a}\mathsf{d}\mathsf{d}$$ $$\frac{}{C⊢\mathsf{i}32.\mathsf{a}\mathsf{d}\mathsf{d}:[\mathsf{i}32\mathsf{i}32]\to [\mathsf{i}32]}$$ $$[\mathsf{i}32\mathsf{i}32]\to [\mathsf{i}32$$ $$\mathsf{i}32$$ can be typed as follows:class="">$$\mathsf{g}\mathsf{e}\mathsf{t}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}$$ $$\frac{C.\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{s}[x]=t}{C⊢\mathsf{g}\mathsf{e}\mathsf{t}\_\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}x:[]\to [t]}$$ local index exists in the context. The instruction produces a value of its respective type $$x$$ $$t$$ does not exist then the premise does noclass="">$$C.\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{a}\mathsf{l}\mathsf{s}[x]$$ structured instruction requires a recursive rule, where the premise is itself a typing judgement:

  $$\frac{C,\mathsf{l}\mathsf{a}\mathsf{b}\mathsf{e}\mathsf{l}[t^{?}]⊢{instr}^{\ast }:[]\to [t^{?}]}{C⊢\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}[t^{?}]{instr}^{\ast }\mathsf{e}\mathsf{n}\mathsf{d}:[]\to [t^{?}]}$$ instruction is only valid whenclass="">$$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$ <��s annotation . If so, then the $$[t^{?}]$$ $$\mathsf{b}\mathsf{l}\mathsf{o}\mathsf{c}\mathsf{k}$$ with the additional label information for the premise.

  $$C$$

  [1]

  The semantics is derived from the following article: Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. Bringing the Web up to Speed with WebAssembly. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.

  [2]	For example: Benjamin Pierce. Types and Programming Languages. The MIT Press 2002

  3.2. Types

  Most types are universally valid. However, restrictions apply to function types as well as the limits of table types and memory types, which must be checked during validation.

  3.2.1. Limits

  Limits must have meaningful bounds.

  3.2.1.1. $$\{\mathsf{m}\mathsf{i}\mathsf{n}n,\mathsf{m}\mathsf{a}\mathsf{x}{m}^{?}\}$$ <">

  If the maximum is not empty, then its value must not be smaller than .

  Then the limit is valid. $$m^{?}$$ $$n$$ $$\frac{(n\le m{)}^{?}}{⊢\{\mathsf{m}\mathsf{i}\mathsf{n}n,\mathsf{m}\mathsf{a}\mathsf{x}{m}^{?}\}ok}$$ <

  3.2.2. Function Types

  Function types may not specify more than one result.

  3.2.2.1. $$[t_1^n]\to [t_2^m]$$ must not be larger than .

  Then the function type is valid.

$$m$$ $$1$$ $$\frac{}{⊢[t_1^{\ast }]\to [t_2^{?}]ok}$$

3.2.3. Table Types

3.2.3.1. $$limitselemtype$$

The limits must be valid$$limits$$

$$\frac{⊢limitsok}{⊢limitselemtypeok}$$ <

3.2.4. Memory Types

3.2.4.1. $$limits$$ must be valid$$limits$$

$$\frac{⊢limitsok}{⊢limitsok}$$ <

3.2.5. Global Types

3.2.5.1. $$mutvaltype$$ <

The global type is valid.

$$\frac{}{⊢mutvaltypeok}$$ <

3.3. Instructions

Instructions are classified by function types that describe how they manipulate the $$[t_1^{\ast }]\to [t_2^{\ast }]$$ that an instruction pops off and the provided output stack with result values of types that it pushes class="">$$t_1^{\ast }$$

Note

class="">$$t_2^{\ast }$$ has type $$\mathsf{i}32.\mathsf{a}\mathsf{d}\mathsf{d}$$ $$[\mathsf{i}32\mathsf{i}32]\to [\mathsf{i}32]$$ $$\mathsf{i}32$$ . Such a sequence has a $${instr}^{\ast }$$ if the accumulative effect of executing the instructions is consuming vclass="">$$[t_1^{\ast }]\to [t_2^{\ast }]$$ .

For some inclass="">$$t_1^{\ast }$$ $$t_2^{\ast }$$ < are called polymorphic. Two degrees of polymorphism can be distinguished:

• value-polymorphic: the value type of one or several individual operands is unconstrained. That is the case for all $$t$$ <>parametric instructions like and $$\mathsf{d}\mathsf{r}\mathsf{o}\mathsf{p}$$ $$\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ of the instruction is unconstrained. That is the case for all $$[t_1^{\ast }]\to [t_2^{\ast }]$$ that perform an unconditional control transfer, such as , $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ $$\mathsf{b}\mathsf{r}$$ $$\mathsf{b}\mathsf{r}\_\mathsf{t}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ $$\mathsf{r}\mathsf{e}\mathsf{t}\mathsf{u}\mathsf{r}\mathsf{n}$$

  Note

  For example, the instruction is valid with type $$\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ , for any possible $$[tt\mathsf{i}32]\to [t]$$

  $$t$$ $$(\mathsf{i}32.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}1)(\mathsf{i}32.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}2)(\mathsf{i}32.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}3)\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ $$(\mathsf{f}64.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}1.0)(\mathsf{f}64.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}2.0)(\mathsf{i}32.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}3)\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ being instantiated to $$t$$ $$\mathsf{s}\mathsf{e}\mathsf{l}\mathsf{e}\mathsf{c}\mathsf{t}$$ , reclass="">$$\mathsf{i}32$$ $$\mathsf{f}64$$ $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ $$[t_1^{\ast }]\to [t_2^{\ast }]$$ $$t_1^{\ast }$$ $$t_2^{\ast }$$ $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}\mathsf{i}32.\mathsf{a}\mathsf{d}\mathsf{d}$$ $$[]\to [\mathsf{i}32\mathsf{i}32]$$ $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$ $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}(\mathsf{i}64.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}0)\mathsf{i}32.\mathsf{a}\mathsf{d}\mathsf{d}$$ instruction that would make the sequence well-typed.

  $$\mathsf{u}\mathsf{n}\mathsf{r}\mathsf{e}\mathsf{a}\mathsf{c}\mathsf{h}\mathsf{a}\mathsf{b}\mathsf{l}\mathsf{e}$$

  3.3.1. Numeric Instructions

  3.3.1.1. $$t.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}c$$ .

$$[]\to [t]$$ $$\frac{}{C⊢t.\mathsf{c}\mathsf{o}\mathsf{n}\mathsf{s}\mathsf{t}c:[]\to [t]}$$ <2" id="-tmathsfhref-syntax-instructionshtmlsyntax-unopmathitunop">3.3.1.2. $$t.unop$$ .